<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><link rel="stylesheet" type="text/css" href="style.css" /><script type="text/javascript" src="highlight.js"></script></head><body><pre><span class="hs-pragma">{-# LANGUAGE DeriveGeneric          #-}</span><span>
</span><span id="line-2"></span><span class="hs-pragma">{-# LANGUAGE TypeOperators          #-}</span><span>
</span><span id="line-3"></span><span class="hs-pragma">{-# LANGUAGE GADTs                  #-}</span><span>
</span><span id="line-4"></span><span class="hs-pragma">{-# LANGUAGE FlexibleInstances      #-}</span><span>
</span><span id="line-5"></span><span class="hs-pragma">{-# LANGUAGE StandaloneDeriving     #-}</span><span>
</span><span id="line-6"></span><span class="hs-pragma">{-# LANGUAGE NoImplicitPrelude      #-}</span><span>
</span><span id="line-7"></span><span class="hs-pragma">{-# LANGUAGE RankNTypes             #-}</span><span>
</span><span id="line-8"></span><span class="hs-pragma">{-# LANGUAGE TypeFamilies           #-}</span><span>
</span><span id="line-9"></span><span class="hs-pragma">{-# LANGUAGE UndecidableInstances   #-}</span><span>
</span><span id="line-10"></span><span class="hs-pragma">{-# LANGUAGE ExplicitNamespaces     #-}</span><span>
</span><span id="line-11"></span><span class="hs-pragma">{-# LANGUAGE MultiParamTypeClasses  #-}</span><span>
</span><span id="line-12"></span><span class="hs-pragma">{-# LANGUAGE FunctionalDependencies #-}</span><span>
</span><span id="line-13"></span><span class="hs-pragma">{-# LANGUAGE DataKinds              #-}</span><span>
</span><span id="line-14"></span><span class="hs-pragma">{-# LANGUAGE PolyKinds              #-}</span><span>
</span><span id="line-15"></span><span class="hs-pragma">{-# LANGUAGE StandaloneKindSignatures #-}</span><span>
</span><span id="line-16"></span><span class="hs-pragma">{-# LANGUAGE Trustworthy            #-}</span><span>
</span><span id="line-17"></span><span>
</span><span id="line-18"></span><span class="hs-comment">-----------------------------------------------------------------------------</span><span>
</span><span id="line-19"></span><span class="hs-comment">-- |</span><span>
</span><span id="line-20"></span><span class="hs-comment">-- Module      :  Data.Type.Equality</span><span>
</span><span id="line-21"></span><span class="hs-comment">-- License     :  BSD-style (see the LICENSE file in the distribution)</span><span>
</span><span id="line-22"></span><span class="hs-comment">--</span><span>
</span><span id="line-23"></span><span class="hs-comment">-- Maintainer  :  libraries@haskell.org</span><span>
</span><span id="line-24"></span><span class="hs-comment">-- Stability   :  experimental</span><span>
</span><span id="line-25"></span><span class="hs-comment">-- Portability :  not portable</span><span>
</span><span id="line-26"></span><span class="hs-comment">--</span><span>
</span><span id="line-27"></span><span class="hs-comment">-- Definition of propositional equality @(':~:')@. Pattern-matching on a variable</span><span>
</span><span id="line-28"></span><span class="hs-comment">-- of type @(a ':~:' b)@ produces a proof that @a '~' b@.</span><span>
</span><span id="line-29"></span><span class="hs-comment">--</span><span>
</span><span id="line-30"></span><span class="hs-comment">-- @since 4.7.0.0</span><span>
</span><span id="line-31"></span><span class="hs-comment">-----------------------------------------------------------------------------</span><span>
</span><span id="line-32"></span><span>
</span><span id="line-33"></span><span>
</span><span id="line-34"></span><span>
</span><span id="line-35"></span><span class="hs-keyword">module</span><span> </span><span class="hs-identifier">Data.Type.Equality</span><span> </span><span class="hs-special">(</span><span>
</span><span id="line-36"></span><span>  </span><span class="annot"><span class="hs-comment">-- * The equality types</span></span><span>
</span><span id="line-37"></span><span>  </span><span class="annot"><a href="Data.Type.Equality.html#%3A~%3A"><span class="hs-operator">(:~:)</span></a></span><span class="hs-special">(</span><span class="hs-glyph">..</span><span class="hs-special">)</span><span class="hs-special">,</span><span> </span><span class="hs-keyword">type</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#~~"><span class="hs-operator">(~~)</span></a></span><span class="hs-special">,</span><span>
</span><span id="line-38"></span><span>  </span><span class="annot"><a href="Data.Type.Equality.html#%3A~~%3A"><span class="hs-operator">(:~~:)</span></a></span><span class="hs-special">(</span><span class="hs-glyph">..</span><span class="hs-special">)</span><span class="hs-special">,</span><span>
</span><span id="line-39"></span><span>
</span><span id="line-40"></span><span>  </span><span class="annot"><span class="hs-comment">-- * Working with equality</span></span><span>
</span><span id="line-41"></span><span>  </span><span class="annot"><a href="Data.Type.Equality.html#sym"><span class="hs-identifier">sym</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><a href="Data.Type.Equality.html#trans"><span class="hs-identifier">trans</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><a href="Data.Type.Equality.html#castWith"><span class="hs-identifier">castWith</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><a href="Data.Type.Equality.html#gcastWith"><span class="hs-identifier">gcastWith</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><a href="Data.Type.Equality.html#apply"><span class="hs-identifier">apply</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><a href="Data.Type.Equality.html#inner"><span class="hs-identifier">inner</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><a href="Data.Type.Equality.html#outer"><span class="hs-identifier">outer</span></a></span><span class="hs-special">,</span><span>
</span><span id="line-42"></span><span>
</span><span id="line-43"></span><span>  </span><span class="annot"><span class="hs-comment">-- * Inferring equality from other types</span></span><span>
</span><span id="line-44"></span><span>  </span><span class="annot"><a href="Data.Type.Equality.html#TestEquality"><span class="hs-identifier">TestEquality</span></a></span><span class="hs-special">(</span><span class="hs-glyph">..</span><span class="hs-special">)</span><span class="hs-special">,</span><span>
</span><span id="line-45"></span><span>
</span><span id="line-46"></span><span>  </span><span class="annot"><span class="hs-comment">-- * Boolean type-level equality</span></span><span>
</span><span id="line-47"></span><span>  </span><span class="hs-keyword">type</span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3D%3D"><span class="hs-operator">(==)</span></a></span><span>
</span><span id="line-48"></span><span>  </span><span class="hs-special">)</span><span> </span><span class="hs-keyword">where</span><span>
</span><span id="line-49"></span><span>
</span><span id="line-50"></span><span class="hs-keyword">import</span><span> </span><span class="annot"><a href="Data.Maybe.html"><span class="hs-identifier">Data.Maybe</span></a></span><span>
</span><span id="line-51"></span><span class="hs-keyword">import</span><span> </span><span class="annot"><a href="GHC.Enum.html"><span class="hs-identifier">GHC.Enum</span></a></span><span>
</span><span id="line-52"></span><span class="hs-keyword">import</span><span> </span><span class="annot"><a href="GHC.Show.html"><span class="hs-identifier">GHC.Show</span></a></span><span>
</span><span id="line-53"></span><span class="hs-keyword">import</span><span> </span><span class="annot"><a href="GHC.Read.html"><span class="hs-identifier">GHC.Read</span></a></span><span>
</span><span id="line-54"></span><span class="hs-keyword">import</span><span> </span><span class="annot"><a href="GHC.Base.html"><span class="hs-identifier">GHC.Base</span></a></span><span>
</span><span id="line-55"></span><span class="hs-keyword">import</span><span> </span><span class="annot"><a href="Data.Type.Bool.html"><span class="hs-identifier">Data.Type.Bool</span></a></span><span>
</span><span id="line-56"></span><span>
</span><span id="line-57"></span><span class="hs-keyword">infix</span><span> </span><span class="hs-number">4</span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~%3A"><span class="hs-operator hs-type">:~:</span></a></span><span class="hs-special">,</span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~~%3A"><span class="hs-operator hs-type">:~~:</span></a></span><span>
</span><span id="line-58"></span><span>
</span><span id="line-59"></span><span class="hs-comment">-- | Propositional equality. If @a :~: b@ is inhabited by some terminating</span><span>
</span><span id="line-60"></span><span class="hs-comment">-- value, then the type @a@ is the same as the type @b@. To use this equality</span><span>
</span><span id="line-61"></span><span class="hs-comment">-- in practice, pattern-match on the @a :~: b@ to get out the @Refl@ constructor;</span><span>
</span><span id="line-62"></span><span class="hs-comment">-- in the body of the pattern-match, the compiler knows that @a ~ b@.</span><span>
</span><span id="line-63"></span><span class="hs-comment">--</span><span>
</span><span id="line-64"></span><span class="hs-comment">-- @since 4.7.0.0</span><span>
</span><span id="line-65"></span><span class="hs-keyword">data</span><span> </span><span id="local-6989586621679506231"><span class="annot"><a href="#local-6989586621679506231"><span class="hs-identifier hs-type">a</span></a></span></span><span> </span><span id="%3A~%3A"><span class="annot"><a href="Data.Type.Equality.html#%3A~%3A"><span class="hs-operator hs-var">:~:</span></a></span></span><span> </span><span id="local-6989586621679506230"><span class="annot"><a href="#local-6989586621679506230"><span class="hs-identifier hs-type">b</span></a></span></span><span> </span><span class="hs-keyword">where</span><span>  </span><span class="hs-comment">-- See Note [The equality types story] in GHC.Builtin.Types.Prim</span><span>
</span><span id="line-66"></span><span>  </span><span id="local-6989586621679506465"><span id="Refl"><span class="annot"><a href="Data.Type.Equality.html#Refl"><span class="hs-identifier hs-var">Refl</span></a></span></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="#local-6989586621679506465"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~%3A"><span class="hs-operator hs-type">:~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506465"><span class="hs-identifier hs-type">a</span></a></span></span><span>
</span><span id="line-67"></span><span>
</span><span id="line-68"></span><span class="hs-comment">-- with credit to Conal Elliott for 'ty', Erik Hesselink &amp; Martijn van</span><span>
</span><span id="line-69"></span><span class="hs-comment">-- Steenbergen for 'type-equality', Edward Kmett for 'eq', and Gabor Greif</span><span>
</span><span id="line-70"></span><span class="hs-comment">-- for 'type-eq'</span><span>
</span><span id="line-71"></span><span>
</span><span id="line-72"></span><span class="hs-comment">-- | Symmetry of equality</span><span>
</span><span id="line-73"></span><span id="local-6989586621679506470"><span id="local-6989586621679506471"><span class="annot"><a href="Data.Type.Equality.html#sym"><span class="hs-identifier hs-type">sym</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679506471"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~%3A"><span class="hs-operator hs-type">:~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506470"><span class="hs-identifier hs-type">b</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679506470"><span class="hs-identifier hs-type">b</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~%3A"><span class="hs-operator hs-type">:~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506471"><span class="hs-identifier hs-type">a</span></a></span><span class="hs-special">)</span></span></span><span>
</span><span id="line-74"></span><span id="sym"><span class="annot"><span class="annottext">sym :: forall {k} (a :: k) (b :: k). (a :~: b) -&gt; b :~: a
</span><a href="Data.Type.Equality.html#sym"><span class="hs-identifier hs-var hs-var">sym</span></a></span></span><span> </span><span class="annot"><span class="annottext">a :~: b
</span><a href="Data.Type.Equality.html#Refl"><span class="hs-identifier hs-var">Refl</span></a></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">b :~: a
forall {k} (a :: k). a :~: a
</span><a href="Data.Type.Equality.html#Refl"><span class="hs-identifier hs-var">Refl</span></a></span><span>
</span><span id="line-75"></span><span>
</span><span id="line-76"></span><span class="hs-comment">-- | Transitivity of equality</span><span>
</span><span id="line-77"></span><span id="local-6989586621679506461"><span id="local-6989586621679506462"><span id="local-6989586621679506463"><span class="annot"><a href="Data.Type.Equality.html#trans"><span class="hs-identifier hs-type">trans</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679506463"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~%3A"><span class="hs-operator hs-type">:~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506462"><span class="hs-identifier hs-type">b</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679506462"><span class="hs-identifier hs-type">b</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~%3A"><span class="hs-operator hs-type">:~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506461"><span class="hs-identifier hs-type">c</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679506463"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~%3A"><span class="hs-operator hs-type">:~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506461"><span class="hs-identifier hs-type">c</span></a></span><span class="hs-special">)</span></span></span></span><span>
</span><span id="line-78"></span><span id="trans"><span class="annot"><span class="annottext">trans :: forall {k} (a :: k) (b :: k) (c :: k).
(a :~: b) -&gt; (b :~: c) -&gt; a :~: c
</span><a href="Data.Type.Equality.html#trans"><span class="hs-identifier hs-var hs-var">trans</span></a></span></span><span> </span><span class="annot"><span class="annottext">a :~: b
</span><a href="Data.Type.Equality.html#Refl"><span class="hs-identifier hs-var">Refl</span></a></span><span> </span><span class="annot"><span class="annottext">b :~: c
</span><a href="Data.Type.Equality.html#Refl"><span class="hs-identifier hs-var">Refl</span></a></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">a :~: c
forall {k} (a :: k). a :~: a
</span><a href="Data.Type.Equality.html#Refl"><span class="hs-identifier hs-var">Refl</span></a></span><span>
</span><span id="line-79"></span><span>
</span><span id="line-80"></span><span class="hs-comment">-- | Type-safe cast, using propositional equality</span><span>
</span><span id="line-81"></span><span id="local-6989586621679506455"><span id="local-6989586621679506456"><span class="annot"><a href="Data.Type.Equality.html#castWith"><span class="hs-identifier hs-type">castWith</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679506456"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~%3A"><span class="hs-operator hs-type">:~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506455"><span class="hs-identifier hs-type">b</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="#local-6989586621679506456"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="#local-6989586621679506455"><span class="hs-identifier hs-type">b</span></a></span></span></span><span>
</span><span id="line-82"></span><span id="castWith"><span class="annot"><span class="annottext">castWith :: forall a b. (a :~: b) -&gt; a -&gt; b
</span><a href="Data.Type.Equality.html#castWith"><span class="hs-identifier hs-var hs-var">castWith</span></a></span></span><span> </span><span class="annot"><span class="annottext">a :~: b
</span><a href="Data.Type.Equality.html#Refl"><span class="hs-identifier hs-var">Refl</span></a></span><span> </span><span id="local-6989586621679506223"><span class="annot"><span class="annottext">a
</span><a href="#local-6989586621679506223"><span class="hs-identifier hs-var">x</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">a
b
</span><a href="#local-6989586621679506223"><span class="hs-identifier hs-var">x</span></a></span><span>
</span><span id="line-83"></span><span>
</span><span id="line-84"></span><span class="hs-comment">-- | Generalized form of type-safe cast using propositional equality</span><span>
</span><span id="line-85"></span><span id="local-6989586621679506449"><span id="local-6989586621679506450"><span id="local-6989586621679506451"><span class="annot"><a href="Data.Type.Equality.html#gcastWith"><span class="hs-identifier hs-type">gcastWith</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679506451"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~%3A"><span class="hs-operator hs-type">:~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506450"><span class="hs-identifier hs-type">b</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="hs-special">(</span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679506451"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#~"><span class="hs-operator hs-type">~</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506450"><span class="hs-identifier hs-type">b</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">=&gt;</span><span> </span><span class="annot"><a href="#local-6989586621679506449"><span class="hs-identifier hs-type">r</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="#local-6989586621679506449"><span class="hs-identifier hs-type">r</span></a></span></span></span></span><span>
</span><span id="line-86"></span><span id="gcastWith"><span class="annot"><span class="annottext">gcastWith :: forall {k} (a :: k) (b :: k) r. (a :~: b) -&gt; ((a ~ b) =&gt; r) -&gt; r
</span><a href="Data.Type.Equality.html#gcastWith"><span class="hs-identifier hs-var hs-var">gcastWith</span></a></span></span><span> </span><span class="annot"><span class="annottext">a :~: b
</span><a href="Data.Type.Equality.html#Refl"><span class="hs-identifier hs-var">Refl</span></a></span><span> </span><span id="local-6989586621679506219"><span class="annot"><span class="annottext">(a ~ b) =&gt; r
</span><a href="#local-6989586621679506219"><span class="hs-identifier hs-var">x</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">r
(a ~ b) =&gt; r
</span><a href="#local-6989586621679506219"><span class="hs-identifier hs-var">x</span></a></span><span>
</span><span id="line-87"></span><span>
</span><span id="line-88"></span><span class="hs-comment">-- | Apply one equality to another, respectively</span><span>
</span><span id="line-89"></span><span id="local-6989586621679506439"><span id="local-6989586621679506440"><span id="local-6989586621679506441"><span id="local-6989586621679506442"><span class="annot"><a href="Data.Type.Equality.html#apply"><span class="hs-identifier hs-type">apply</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679506442"><span class="hs-identifier hs-type">f</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~%3A"><span class="hs-operator hs-type">:~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506441"><span class="hs-identifier hs-type">g</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679506440"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~%3A"><span class="hs-operator hs-type">:~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506439"><span class="hs-identifier hs-type">b</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679506442"><span class="hs-identifier hs-type">f</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506440"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~%3A"><span class="hs-operator hs-type">:~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506441"><span class="hs-identifier hs-type">g</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506439"><span class="hs-identifier hs-type">b</span></a></span><span class="hs-special">)</span></span></span></span></span><span>
</span><span id="line-90"></span><span id="apply"><span class="annot"><span class="annottext">apply :: forall {k} {k} (f :: k -&gt; k) (g :: k -&gt; k) (a :: k) (b :: k).
(f :~: g) -&gt; (a :~: b) -&gt; f a :~: g b
</span><a href="Data.Type.Equality.html#apply"><span class="hs-identifier hs-var hs-var">apply</span></a></span></span><span> </span><span class="annot"><span class="annottext">f :~: g
</span><a href="Data.Type.Equality.html#Refl"><span class="hs-identifier hs-var">Refl</span></a></span><span> </span><span class="annot"><span class="annottext">a :~: b
</span><a href="Data.Type.Equality.html#Refl"><span class="hs-identifier hs-var">Refl</span></a></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">f a :~: g b
forall {k} (a :: k). a :~: a
</span><a href="Data.Type.Equality.html#Refl"><span class="hs-identifier hs-var">Refl</span></a></span><span>
</span><span id="line-91"></span><span>
</span><span id="line-92"></span><span class="hs-comment">-- | Extract equality of the arguments from an equality of applied types</span><span>
</span><span id="line-93"></span><span id="local-6989586621679506427"><span id="local-6989586621679506428"><span id="local-6989586621679506429"><span id="local-6989586621679506430"><span class="annot"><a href="Data.Type.Equality.html#inner"><span class="hs-identifier hs-type">inner</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679506430"><span class="hs-identifier hs-type">f</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506429"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~%3A"><span class="hs-operator hs-type">:~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506428"><span class="hs-identifier hs-type">g</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506427"><span class="hs-identifier hs-type">b</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679506429"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~%3A"><span class="hs-operator hs-type">:~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506427"><span class="hs-identifier hs-type">b</span></a></span><span class="hs-special">)</span></span></span></span></span><span>
</span><span id="line-94"></span><span id="inner"><span class="annot"><span class="annottext">inner :: forall {k} {k} (f :: k -&gt; k) (a :: k) (g :: k -&gt; k) (b :: k).
(f a :~: g b) -&gt; a :~: b
</span><a href="Data.Type.Equality.html#inner"><span class="hs-identifier hs-var hs-var">inner</span></a></span></span><span> </span><span class="annot"><span class="annottext">f a :~: g b
</span><a href="Data.Type.Equality.html#Refl"><span class="hs-identifier hs-var">Refl</span></a></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">a :~: b
forall {k} (a :: k). a :~: a
</span><a href="Data.Type.Equality.html#Refl"><span class="hs-identifier hs-var">Refl</span></a></span><span>
</span><span id="line-95"></span><span>
</span><span id="line-96"></span><span class="hs-comment">-- | Extract equality of type constructors from an equality of applied types</span><span>
</span><span id="line-97"></span><span id="local-6989586621679506415"><span id="local-6989586621679506416"><span id="local-6989586621679506417"><span id="local-6989586621679506418"><span class="annot"><a href="Data.Type.Equality.html#outer"><span class="hs-identifier hs-type">outer</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679506418"><span class="hs-identifier hs-type">f</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506417"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~%3A"><span class="hs-operator hs-type">:~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506416"><span class="hs-identifier hs-type">g</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506415"><span class="hs-identifier hs-type">b</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679506418"><span class="hs-identifier hs-type">f</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~%3A"><span class="hs-operator hs-type">:~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506416"><span class="hs-identifier hs-type">g</span></a></span><span class="hs-special">)</span></span></span></span></span><span>
</span><span id="line-98"></span><span id="outer"><span class="annot"><span class="annottext">outer :: forall {k} {k} (f :: k -&gt; k) (a :: k) (g :: k -&gt; k) (b :: k).
(f a :~: g b) -&gt; f :~: g
</span><a href="Data.Type.Equality.html#outer"><span class="hs-identifier hs-var hs-var">outer</span></a></span></span><span> </span><span class="annot"><span class="annottext">f a :~: g b
</span><a href="Data.Type.Equality.html#Refl"><span class="hs-identifier hs-var">Refl</span></a></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">f :~: g
forall {k} (a :: k). a :~: a
</span><a href="Data.Type.Equality.html#Refl"><span class="hs-identifier hs-var">Refl</span></a></span><span>
</span><span id="line-99"></span><span>
</span><span id="line-100"></span><span class="hs-comment">-- | @since 4.7.0.0</span><span>
</span><span id="line-101"></span><span id="local-6989586621679506209"><span id="local-6989586621679506211"><span id="local-6989586621679506405"><span id="local-6989586621679506406"><span class="hs-keyword">deriving</span><span> </span><span class="hs-keyword">instance</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Classes.html#Eq"><span class="hs-identifier hs-type">Eq</span></a></span><span>   </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679506406"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~%3A"><span class="hs-operator hs-type">:~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506405"><span class="hs-identifier hs-type">b</span></a></span><span class="hs-special">)</span></span></span></span></span><span>
</span><span id="line-102"></span><span>
</span><span id="line-103"></span><span class="hs-comment">-- | @since 4.7.0.0</span><span>
</span><span id="line-104"></span><span id="local-6989586621679506202"><span id="local-6989586621679506204"><span id="local-6989586621679506206"><span id="local-6989586621679506400"><span id="local-6989586621679506401"><span class="hs-keyword">deriving</span><span> </span><span class="hs-keyword">instance</span><span> </span><span class="annot"><a href="GHC.Show.html#Show"><span class="hs-identifier hs-type">Show</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679506401"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~%3A"><span class="hs-operator hs-type">:~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506400"><span class="hs-identifier hs-type">b</span></a></span><span class="hs-special">)</span></span></span></span></span></span><span>
</span><span id="line-105"></span><span>
</span><span id="line-106"></span><span class="hs-comment">-- | @since 4.7.0.0</span><span>
</span><span id="line-107"></span><span id="local-6989586621679506182"><span id="local-6989586621679506184"><span id="local-6989586621679506187"><span id="local-6989586621679506190"><span id="local-6989586621679506193"><span id="local-6989586621679506195"><span id="local-6989586621679506197"><span id="local-6989586621679506396"><span id="local-6989586621679506397"><span class="hs-keyword">deriving</span><span> </span><span class="hs-keyword">instance</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Classes.html#Ord"><span class="hs-identifier hs-type">Ord</span></a></span><span>  </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679506397"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~%3A"><span class="hs-operator hs-type">:~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506396"><span class="hs-identifier hs-type">b</span></a></span><span class="hs-special">)</span></span></span></span></span></span></span></span></span></span><span>
</span><span id="line-108"></span><span>
</span><span id="line-109"></span><span class="hs-comment">-- | @since 4.7.0.0</span><span>
</span><span id="line-110"></span><span id="local-6989586621679506168"><span id="local-6989586621679506173"><span id="local-6989586621679506177"><span id="local-6989586621679506179"><span id="local-6989586621679506390"><span id="local-6989586621679506391"><span class="hs-keyword">deriving</span><span> </span><span class="hs-keyword">instance</span><span> </span><span class="annot"><a href="#local-6989586621679506391"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#~"><span class="hs-operator hs-type">~</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506390"><span class="hs-identifier hs-type">b</span></a></span><span> </span><span class="hs-glyph">=&gt;</span><span> </span><span class="annot"><a href="GHC.Read.html#Read"><span class="hs-identifier hs-type">Read</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679506391"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~%3A"><span class="hs-operator hs-type">:~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506390"><span class="hs-identifier hs-type">b</span></a></span><span class="hs-special">)</span></span></span></span></span></span></span><span>
</span><span id="line-111"></span><span>
</span><span id="line-112"></span><span class="hs-comment">-- | @since 4.7.0.0</span><span>
</span><span id="line-113"></span><span id="local-6989586621679506386"><span id="local-6989586621679506387"><span class="hs-keyword">instance</span><span> </span><span id="local-6989586621679506151"><span id="local-6989586621679506153"><span id="local-6989586621679506155"><span id="local-6989586621679506157"><span id="local-6989586621679506161"><span id="local-6989586621679506163"><span class="annot"><a href="#local-6989586621679506387"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#~"><span class="hs-operator hs-type">~</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506386"><span class="hs-identifier hs-type">b</span></a></span><span> </span><span class="hs-glyph">=&gt;</span><span> </span><span class="annot"><a href="GHC.Enum.html#Enum"><span class="hs-identifier hs-type">Enum</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679506387"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~%3A"><span class="hs-operator hs-type">:~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506386"><span class="hs-identifier hs-type">b</span></a></span><span class="hs-special">)</span></span></span></span></span></span></span><span> </span><span class="hs-keyword">where</span><span>
</span><span id="line-114"></span><span>  </span><span id="local-6989586621679506145"><span class="annot"><span class="annottext">toEnum :: Int -&gt; a :~: b
</span><a href="GHC.Enum.html#toEnum"><span class="hs-identifier hs-var hs-var hs-var hs-var">toEnum</span></a></span></span><span> </span><span class="annot"><span class="annottext">Int
</span><span class="hs-number">0</span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">a :~: b
forall {k} (a :: k). a :~: a
</span><a href="Data.Type.Equality.html#Refl"><span class="hs-identifier hs-var">Refl</span></a></span><span>
</span><span id="line-115"></span><span>  </span><span class="annot"><a href="GHC.Enum.html#toEnum"><span class="hs-identifier hs-var">toEnum</span></a></span><span> </span><span class="annot"><span class="annottext">Int
</span><span class="hs-identifier">_</span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">String -&gt; a :~: b
forall a. String -&gt; a
</span><a href="GHC.Err.html#errorWithoutStackTrace"><span class="hs-identifier hs-var">errorWithoutStackTrace</span></a></span><span> </span><span class="annot"><span class="annottext">String
</span><span class="hs-string">&quot;Data.Type.Equality.toEnum: bad argument&quot;</span></span><span>
</span><span id="line-116"></span><span>
</span><span id="line-117"></span><span>  </span><span id="local-6989586621679506142"><span class="annot"><span class="annottext">fromEnum :: (a :~: b) -&gt; Int
</span><a href="GHC.Enum.html#fromEnum"><span class="hs-identifier hs-var hs-var hs-var hs-var">fromEnum</span></a></span></span><span> </span><span class="annot"><span class="annottext">a :~: b
</span><a href="Data.Type.Equality.html#Refl"><span class="hs-identifier hs-var">Refl</span></a></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">Int
</span><span class="hs-number">0</span></span></span></span><span>
</span><span id="line-118"></span><span>
</span><span id="line-119"></span><span class="hs-comment">-- | @since 4.7.0.0</span><span>
</span><span id="line-120"></span><span id="local-6989586621679506135"><span id="local-6989586621679506137"><span id="local-6989586621679506377"><span id="local-6989586621679506378"><span class="hs-keyword">deriving</span><span> </span><span class="hs-keyword">instance</span><span> </span><span class="annot"><a href="#local-6989586621679506378"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#~"><span class="hs-operator hs-type">~</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506377"><span class="hs-identifier hs-type">b</span></a></span><span> </span><span class="hs-glyph">=&gt;</span><span> </span><span class="annot"><a href="GHC.Enum.html#Bounded"><span class="hs-identifier hs-type">Bounded</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679506378"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~%3A"><span class="hs-operator hs-type">:~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506377"><span class="hs-identifier hs-type">b</span></a></span><span class="hs-special">)</span></span></span></span></span><span>
</span><span id="line-121"></span><span>
</span><span id="line-122"></span><span class="hs-comment">-- | Kind heterogeneous propositional equality. Like ':~:', @a :~~: b@ is</span><span>
</span><span id="line-123"></span><span class="hs-comment">-- inhabited by a terminating value if and only if @a@ is the same type as @b@.</span><span>
</span><span id="line-124"></span><span class="hs-comment">--</span><span>
</span><span id="line-125"></span><span class="hs-comment">-- @since 4.10.0.0</span><span>
</span><span id="line-126"></span><span id="local-6989586621679506130"><span id="local-6989586621679506131"><span class="hs-keyword">type</span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~~%3A"><span class="hs-operator hs-type">(:~~:)</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="#local-6989586621679506131"><span class="hs-identifier hs-type">k1</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="#local-6989586621679506130"><span class="hs-identifier hs-type">k2</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Type"><span class="hs-identifier hs-type">Type</span></a></span></span></span><span>
</span><span id="line-127"></span><span class="hs-keyword">data</span><span> </span><span id="local-6989586621679506129"><span class="annot"><a href="#local-6989586621679506129"><span class="hs-identifier hs-type">a</span></a></span></span><span> </span><span id="%3A~~%3A"><span class="annot"><a href="Data.Type.Equality.html#%3A~~%3A"><span class="hs-operator hs-var">:~~:</span></a></span></span><span> </span><span id="local-6989586621679506128"><span class="annot"><a href="#local-6989586621679506128"><span class="hs-identifier hs-type">b</span></a></span></span><span> </span><span class="hs-keyword">where</span><span>
</span><span id="line-128"></span><span>   </span><span id="local-6989586621679506355"><span id="HRefl"><span class="annot"><a href="Data.Type.Equality.html#HRefl"><span class="hs-identifier hs-var">HRefl</span></a></span></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="#local-6989586621679506355"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~~%3A"><span class="hs-operator hs-type">:~~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506355"><span class="hs-identifier hs-type">a</span></a></span></span><span>
</span><span id="line-129"></span><span>
</span><span id="line-130"></span><span class="hs-comment">-- | @since 4.10.0.0</span><span>
</span><span id="line-131"></span><span id="local-6989586621679506123"><span id="local-6989586621679506125"><span id="local-6989586621679506373"><span id="local-6989586621679506374"><span class="hs-keyword">deriving</span><span> </span><span class="hs-keyword">instance</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Classes.html#Eq"><span class="hs-identifier hs-type">Eq</span></a></span><span>   </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679506374"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~~%3A"><span class="hs-operator hs-type">:~~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506373"><span class="hs-identifier hs-type">b</span></a></span><span class="hs-special">)</span></span></span></span></span><span>
</span><span id="line-132"></span><span class="hs-comment">-- | @since 4.10.0.0</span><span>
</span><span id="line-133"></span><span id="local-6989586621679506117"><span id="local-6989586621679506119"><span id="local-6989586621679506121"><span id="local-6989586621679506369"><span id="local-6989586621679506370"><span class="hs-keyword">deriving</span><span> </span><span class="hs-keyword">instance</span><span> </span><span class="annot"><a href="GHC.Show.html#Show"><span class="hs-identifier hs-type">Show</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679506370"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~~%3A"><span class="hs-operator hs-type">:~~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506369"><span class="hs-identifier hs-type">b</span></a></span><span class="hs-special">)</span></span></span></span></span></span><span>
</span><span id="line-134"></span><span class="hs-comment">-- | @since 4.10.0.0</span><span>
</span><span id="line-135"></span><span id="local-6989586621679506098"><span id="local-6989586621679506100"><span id="local-6989586621679506103"><span id="local-6989586621679506106"><span id="local-6989586621679506109"><span id="local-6989586621679506111"><span id="local-6989586621679506113"><span id="local-6989586621679506365"><span id="local-6989586621679506366"><span class="hs-keyword">deriving</span><span> </span><span class="hs-keyword">instance</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Classes.html#Ord"><span class="hs-identifier hs-type">Ord</span></a></span><span>  </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679506366"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~~%3A"><span class="hs-operator hs-type">:~~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506365"><span class="hs-identifier hs-type">b</span></a></span><span class="hs-special">)</span></span></span></span></span></span></span></span></span></span><span>
</span><span id="line-136"></span><span>
</span><span id="line-137"></span><span class="hs-comment">-- | @since 4.10.0.0</span><span>
</span><span id="line-138"></span><span id="local-6989586621679506086"><span id="local-6989586621679506090"><span id="local-6989586621679506094"><span id="local-6989586621679506096"><span id="local-6989586621679506361"><span id="local-6989586621679506362"><span class="hs-keyword">deriving</span><span> </span><span class="hs-keyword">instance</span><span> </span><span class="annot"><a href="#local-6989586621679506362"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#~~"><span class="hs-operator hs-type">~~</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506361"><span class="hs-identifier hs-type">b</span></a></span><span> </span><span class="hs-glyph">=&gt;</span><span> </span><span class="annot"><a href="GHC.Read.html#Read"><span class="hs-identifier hs-type">Read</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679506362"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~~%3A"><span class="hs-operator hs-type">:~~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506361"><span class="hs-identifier hs-type">b</span></a></span><span class="hs-special">)</span></span></span></span></span></span></span><span>
</span><span id="line-139"></span><span>
</span><span id="line-140"></span><span class="hs-comment">-- | @since 4.10.0.0</span><span>
</span><span id="line-141"></span><span id="local-6989586621679506357"><span id="local-6989586621679506358"><span class="hs-keyword">instance</span><span> </span><span id="local-6989586621679506070"><span id="local-6989586621679506072"><span id="local-6989586621679506074"><span id="local-6989586621679506076"><span id="local-6989586621679506080"><span id="local-6989586621679506082"><span class="annot"><a href="#local-6989586621679506358"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#~~"><span class="hs-operator hs-type">~~</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506357"><span class="hs-identifier hs-type">b</span></a></span><span> </span><span class="hs-glyph">=&gt;</span><span> </span><span class="annot"><a href="GHC.Enum.html#Enum"><span class="hs-identifier hs-type">Enum</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679506358"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~~%3A"><span class="hs-operator hs-type">:~~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506357"><span class="hs-identifier hs-type">b</span></a></span><span class="hs-special">)</span></span></span></span></span></span></span><span> </span><span class="hs-keyword">where</span><span>
</span><span id="line-142"></span><span>  </span><span id="local-6989586621679506067"><span class="annot"><span class="annottext">toEnum :: Int -&gt; a :~~: b
</span><a href="#local-6989586621679506067"><span class="hs-identifier hs-var hs-var hs-var hs-var">toEnum</span></a></span></span><span> </span><span class="annot"><span class="annottext">Int
</span><span class="hs-number">0</span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">a :~~: b
forall {k2} (a :: k2). a :~~: a
</span><a href="Data.Type.Equality.html#HRefl"><span class="hs-identifier hs-var">HRefl</span></a></span><span>
</span><span id="line-143"></span><span>  </span><span class="annot"><a href="GHC.Enum.html#toEnum"><span class="hs-identifier hs-var">toEnum</span></a></span><span> </span><span class="annot"><span class="annottext">Int
</span><span class="hs-identifier">_</span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">String -&gt; a :~~: b
forall a. String -&gt; a
</span><a href="GHC.Err.html#errorWithoutStackTrace"><span class="hs-identifier hs-var">errorWithoutStackTrace</span></a></span><span> </span><span class="annot"><span class="annottext">String
</span><span class="hs-string">&quot;Data.Type.Equality.toEnum: bad argument&quot;</span></span><span>
</span><span id="line-144"></span><span>
</span><span id="line-145"></span><span>  </span><span id="local-6989586621679506066"><span class="annot"><span class="annottext">fromEnum :: (a :~~: b) -&gt; Int
</span><a href="#local-6989586621679506066"><span class="hs-identifier hs-var hs-var hs-var hs-var">fromEnum</span></a></span></span><span> </span><span class="annot"><span class="annottext">a :~~: b
</span><a href="Data.Type.Equality.html#HRefl"><span class="hs-identifier hs-var">HRefl</span></a></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">Int
</span><span class="hs-number">0</span></span></span></span><span>
</span><span id="line-146"></span><span>
</span><span id="line-147"></span><span class="hs-comment">-- | @since 4.10.0.0</span><span>
</span><span id="line-148"></span><span id="local-6989586621679506059"><span id="local-6989586621679506061"><span id="local-6989586621679506347"><span id="local-6989586621679506348"><span class="hs-keyword">deriving</span><span> </span><span class="hs-keyword">instance</span><span> </span><span class="annot"><a href="#local-6989586621679506348"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#~~"><span class="hs-operator hs-type">~~</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506347"><span class="hs-identifier hs-type">b</span></a></span><span> </span><span class="hs-glyph">=&gt;</span><span> </span><span class="annot"><a href="GHC.Enum.html#Bounded"><span class="hs-identifier hs-type">Bounded</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679506348"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~~%3A"><span class="hs-operator hs-type">:~~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506347"><span class="hs-identifier hs-type">b</span></a></span><span class="hs-special">)</span></span></span></span></span><span>
</span><span id="line-149"></span><span>
</span><span id="line-150"></span><span class="hs-comment">-- | This class contains types where you can learn the equality of two types</span><span>
</span><span id="line-151"></span><span class="hs-comment">-- from information contained in /terms/. Typically, only singleton types should</span><span>
</span><span id="line-152"></span><span class="hs-comment">-- inhabit this class.</span><span>
</span><span id="line-153"></span><span class="hs-keyword">class</span><span> </span><span id="TestEquality"><span class="annot"><a href="Data.Type.Equality.html#TestEquality"><span class="hs-identifier hs-var">TestEquality</span></a></span></span><span> </span><span id="local-6989586621679506340"><span class="annot"><a href="#local-6989586621679506340"><span class="hs-identifier hs-type">f</span></a></span></span><span> </span><span class="hs-keyword">where</span><span>
</span><span id="line-154"></span><span>  </span><span class="hs-comment">-- | Conditionally prove the equality of @a@ and @b@.</span><span>
</span><span id="line-155"></span><span>  </span><span id="local-6989586621679506343"><span id="local-6989586621679506344"><span id="testEquality"><span class="annot"><a href="Data.Type.Equality.html#testEquality"><span class="hs-identifier hs-type">testEquality</span></a></span></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="#local-6989586621679506340"><span class="hs-identifier hs-type">f</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506344"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="#local-6989586621679506340"><span class="hs-identifier hs-type">f</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506343"><span class="hs-identifier hs-type">b</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="GHC.Maybe.html#Maybe"><span class="hs-identifier hs-type">Maybe</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="#local-6989586621679506344"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3A~%3A"><span class="hs-operator hs-type">:~:</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506343"><span class="hs-identifier hs-type">b</span></a></span><span class="hs-special">)</span></span></span><span>
</span><span id="line-156"></span><span>
</span><span id="line-157"></span><span class="hs-comment">-- | @since 4.7.0.0</span><span>
</span><span id="line-158"></span><span id="local-6989586621679506338"><span class="hs-keyword">instance</span><span> </span><span class="annot"><a href="Data.Type.Equality.html#TestEquality"><span class="hs-identifier hs-type">TestEquality</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="Data.Type.Equality.html#%3A~%3A"><span class="hs-operator hs-type">(:~:)</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506338"><span class="hs-identifier hs-type">a</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-keyword">where</span><span>
</span><span id="line-159"></span><span>  </span><span id="local-6989586621679506050"><span class="annot"><span class="annottext">testEquality :: forall (a :: k) (b :: k). (a :~: a) -&gt; (a :~: b) -&gt; Maybe (a :~: b)
</span><a href="#local-6989586621679506050"><span class="hs-identifier hs-var hs-var hs-var hs-var">testEquality</span></a></span></span><span> </span><span class="annot"><span class="annottext">a :~: a
</span><a href="Data.Type.Equality.html#Refl"><span class="hs-identifier hs-var">Refl</span></a></span><span> </span><span class="annot"><span class="annottext">a :~: b
</span><a href="Data.Type.Equality.html#Refl"><span class="hs-identifier hs-var">Refl</span></a></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">(a :~: a) -&gt; Maybe (a :~: a)
forall a. a -&gt; Maybe a
</span><a href="GHC.Maybe.html#Just"><span class="hs-identifier hs-var">Just</span></a></span><span> </span><span class="annot"><span class="annottext">a :~: a
forall {k} (a :: k). a :~: a
</span><a href="Data.Type.Equality.html#Refl"><span class="hs-identifier hs-var">Refl</span></a></span></span><span>
</span><span id="line-160"></span><span>
</span><span id="line-161"></span><span class="hs-comment">-- | @since 4.10.0.0</span><span>
</span><span id="line-162"></span><span id="local-6989586621679506329"><span class="hs-keyword">instance</span><span> </span><span class="annot"><a href="Data.Type.Equality.html#TestEquality"><span class="hs-identifier hs-type">TestEquality</span></a></span><span> </span><span class="hs-special">(</span><span class="annot"><a href="Data.Type.Equality.html#%3A~~%3A"><span class="hs-operator hs-type">(:~~:)</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506329"><span class="hs-identifier hs-type">a</span></a></span><span class="hs-special">)</span><span> </span><span class="hs-keyword">where</span><span>
</span><span id="line-163"></span><span>  </span><span id="local-6989586621679506045"><span class="annot"><span class="annottext">testEquality :: forall (a :: k) (b :: k).
(a :~~: a) -&gt; (a :~~: b) -&gt; Maybe (a :~: b)
</span><a href="#local-6989586621679506045"><span class="hs-identifier hs-var hs-var hs-var hs-var">testEquality</span></a></span></span><span> </span><span class="annot"><span class="annottext">a :~~: a
</span><a href="Data.Type.Equality.html#HRefl"><span class="hs-identifier hs-var">HRefl</span></a></span><span> </span><span class="annot"><span class="annottext">a :~~: b
</span><a href="Data.Type.Equality.html#HRefl"><span class="hs-identifier hs-var">HRefl</span></a></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><span class="annottext">(a :~: a) -&gt; Maybe (a :~: a)
forall a. a -&gt; Maybe a
</span><a href="GHC.Maybe.html#Just"><span class="hs-identifier hs-var">Just</span></a></span><span> </span><span class="annot"><span class="annottext">a :~: a
forall {k} (a :: k). a :~: a
</span><a href="Data.Type.Equality.html#Refl"><span class="hs-identifier hs-var">Refl</span></a></span></span><span>
</span><span id="line-164"></span><span>
</span><span id="line-165"></span><span class="hs-keyword">infix</span><span> </span><span class="hs-number">4</span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3D%3D"><span class="hs-operator hs-type">==</span></a></span><span>
</span><span id="line-166"></span><span>
</span><span id="line-167"></span><span class="hs-comment">-- | A type family to compute Boolean equality.</span><span>
</span><span id="line-168"></span><span id="local-6989586621679506036"><span class="hs-keyword">type</span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3D%3D"><span class="hs-operator hs-type">(==)</span></a></span><span> </span><span class="hs-glyph">::</span><span> </span><span class="annot"><a href="#local-6989586621679506036"><span class="hs-identifier hs-type">k</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="#local-6989586621679506036"><span class="hs-identifier hs-type">k</span></a></span><span> </span><span class="hs-glyph">-&gt;</span><span> </span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#Bool"><span class="hs-identifier hs-type">Bool</span></a></span></span><span>
</span><span id="line-169"></span><span class="hs-keyword">type</span><span> </span><span class="hs-keyword">family</span><span> </span><span id="local-6989586621679506035"><span class="annot"><a href="#local-6989586621679506035"><span class="hs-identifier hs-type">a</span></a></span></span><span> </span><span id="%3D%3D"><span class="annot"><a href="Data.Type.Equality.html#%3D%3D"><span class="hs-operator hs-var">==</span></a></span></span><span> </span><span id="local-6989586621679506034"><span class="annot"><a href="#local-6989586621679506034"><span class="hs-identifier hs-type">b</span></a></span></span><span> </span><span class="hs-keyword">where</span><span>
</span><span id="line-170"></span><span>  </span><span id="local-6989586621679506030"><span id="local-6989586621679506031"><span id="local-6989586621679506032"><span id="local-6989586621679506033"><span class="annot"><a href="#local-6989586621679506033"><span class="hs-identifier hs-type">f</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506032"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span id="%3D%3D"><span class="annot"><a href="Data.Type.Equality.html#%3D%3D"><span class="hs-operator hs-var">==</span></a></span></span><span> </span><span class="annot"><a href="#local-6989586621679506031"><span class="hs-identifier hs-type">g</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506030"><span class="hs-identifier hs-type">b</span></a></span></span></span></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="annot"><a href="#local-6989586621679506033"><span class="hs-identifier hs-type">f</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3D%3D"><span class="hs-operator hs-type">==</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506031"><span class="hs-identifier hs-type">g</span></a></span><span> </span><span class="annot"><a href="Data.Type.Bool.html#%26%26"><span class="hs-operator hs-type">&amp;&amp;</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506032"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span class="annot"><a href="Data.Type.Equality.html#%3D%3D"><span class="hs-operator hs-type">==</span></a></span><span> </span><span class="annot"><a href="#local-6989586621679506030"><span class="hs-identifier hs-type">b</span></a></span><span>
</span><span id="line-171"></span><span>  </span><span id="local-6989586621679506028"><span class="annot"><a href="#local-6989586621679506028"><span class="hs-identifier hs-type">a</span></a></span><span> </span><span id="%3D%3D"><span class="annot"><a href="Data.Type.Equality.html#%3D%3D"><span class="hs-operator hs-var">==</span></a></span></span><span> </span><span class="annot"><a href="#local-6989586621679506028"><span class="hs-identifier hs-type">a</span></a></span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="hs-special">'</span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#True"><span class="hs-identifier hs-type">True</span></a></span><span>
</span><span id="line-172"></span><span>  </span><span class="annot"><span class="hs-identifier">_</span></span><span> </span><span id="%3D%3D"><span class="annot"><a href="Data.Type.Equality.html#%3D%3D"><span class="hs-operator hs-var">==</span></a></span></span><span> </span><span class="annot"><span class="hs-identifier">_</span></span><span> </span><span class="hs-glyph">=</span><span> </span><span class="hs-special">'</span><span class="annot"><a href="../../ghc-prim/src/GHC.Types.html#False"><span class="hs-identifier hs-type">False</span></a></span><span>
</span><span id="line-173"></span><span>
</span><span id="line-174"></span><span class="hs-comment">-- The idea here is to recognize equality of *applications* using</span><span>
</span><span id="line-175"></span><span class="hs-comment">-- the first case, and of *constructors* using the second and third</span><span>
</span><span id="line-176"></span><span class="hs-comment">-- ones. It would be wonderful if GHC recognized that the</span><span>
</span><span id="line-177"></span><span class="hs-comment">-- first and second cases are compatible, which would allow us to</span><span>
</span><span id="line-178"></span><span class="hs-comment">-- prove</span><span>
</span><span id="line-179"></span><span class="hs-comment">--</span><span>
</span><span id="line-180"></span><span class="hs-comment">-- a ~ b =&gt; a == b</span><span>
</span><span id="line-181"></span><span class="hs-comment">--</span><span>
</span><span id="line-182"></span><span class="hs-comment">-- but it (understandably) does not.</span><span>
</span><span id="line-183"></span><span class="hs-comment">--</span><span>
</span><span id="line-184"></span><span class="hs-comment">-- It is absolutely critical that the three cases occur in precisely</span><span>
</span><span id="line-185"></span><span class="hs-comment">-- this order. In particular, if</span><span>
</span><span id="line-186"></span><span class="hs-comment">--</span><span>
</span><span id="line-187"></span><span class="hs-comment">-- a == a = 'True</span><span>
</span><span id="line-188"></span><span class="hs-comment">--</span><span>
</span><span id="line-189"></span><span class="hs-comment">-- came first, then the type application case would only be reached</span><span>
</span><span id="line-190"></span><span class="hs-comment">-- (uselessly) when GHC discovered that the types were not equal.</span><span>
</span><span id="line-191"></span><span class="hs-comment">--</span><span>
</span><span id="line-192"></span><span class="hs-comment">-- One might reasonably ask what's wrong with a simpler version:</span><span>
</span><span id="line-193"></span><span class="hs-comment">--</span><span>
</span><span id="line-194"></span><span class="hs-comment">-- type family (a :: k) == (b :: k) where</span><span>
</span><span id="line-195"></span><span class="hs-comment">--  a == a = True</span><span>
</span><span id="line-196"></span><span class="hs-comment">--  a == b = False</span><span>
</span><span id="line-197"></span><span class="hs-comment">--</span><span>
</span><span id="line-198"></span><span class="hs-comment">-- Consider</span><span>
</span><span id="line-199"></span><span class="hs-comment">-- data Nat = Zero | Succ Nat</span><span>
</span><span id="line-200"></span><span class="hs-comment">--</span><span>
</span><span id="line-201"></span><span class="hs-comment">-- Suppose I want</span><span>
</span><span id="line-202"></span><span class="hs-comment">-- foo :: (Succ n == Succ m) ~ True =&gt; ((n == m) :~: True)</span><span>
</span><span id="line-203"></span><span class="hs-comment">-- foo = Refl</span><span>
</span><span id="line-204"></span><span class="hs-comment">--</span><span>
</span><span id="line-205"></span><span class="hs-comment">-- This would not type-check with the simple version. `Succ n == Succ m`</span><span>
</span><span id="line-206"></span><span class="hs-comment">-- is stuck. We don't know enough about `n` and `m` to reduce the family.</span><span>
</span><span id="line-207"></span><span class="hs-comment">-- With the recursive version, `Succ n == Succ m` reduces to</span><span>
</span><span id="line-208"></span><span class="hs-comment">-- `Succ == Succ &amp;&amp; n == m`, which can reduce to `'True &amp;&amp; n == m` and</span><span>
</span><span id="line-209"></span><span class="hs-comment">-- finally to `n == m`.</span><span>
</span><span id="line-210"></span></pre></body></html>